Nuprl Lemma : inject-composes
11,40
postcript
pdf
A
,
B0
,
B1
,
C
:Type,
f
:(
A
B0
),
g
:(
B1
C
).
strong-subtype(
B0
;
B1
)
Inj(
A
;
B0
;
f
)
Inj(
B1
;
C
;
g
)
Inj(
A
;
C
;
g
o
f
)
latex
Definitions
Type
,
t
T
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
strong-subtype(
A
;
B
)
,
Inj(
A
;
B
;
f
)
,
P
Q
,
x
:
A
B
(
x
)
,
A
c
B
,
f
(
a
)
,
s
=
t
,
,
<
a
,
b
>
,
f
o
g
Lemmas
inject
wf
,
strong-subtype
wf
origin
A, B0, B1, C:Type, f:(A
B0), g:(B1C).
Inj(A;B0;f) Inj(B1;C;g) Inj(A;C;g o f) A, B0, B1, C:Type, f:(AB0), g:(B1C).
Inj(A;B0;f) Inj(B1;C;g) Inj(A;C;g o f) 
TB(x)x:A. B(x) Q
B(x)
B